<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue982</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

%\renewcommand{\AgdaIndent}{\;\;}

</a><a id="98" class="Markup">\begin{code}</a>
<a id="111" class="Keyword">record</a> <a id="Sigma"></a><a id="118" href="Issue982.html#118" class="Record">Sigma</a> <a id="124" class="Symbol">(</a><a id="125" href="Issue982.html#125" class="Bound">A</a> <a id="127" class="Symbol">:</a> <a id="129" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="132" class="Symbol">)</a> <a id="134" class="Symbol">(</a><a id="135" href="Issue982.html#135" class="Bound">B</a> <a id="137" class="Symbol">:</a> <a id="139" href="Issue982.html#125" class="Bound">A</a> <a id="141" class="Symbol">→</a> <a id="143" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="146" class="Symbol">)</a> <a id="148" class="Symbol">:</a> <a id="150" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="154" class="Keyword">where</a>
  <a id="162" class="Keyword">constructor</a> <a id="_,_"></a><a id="174" href="Issue982.html#174" class="InductiveConstructor Operator">_,_</a>
  <a id="180" class="Keyword">field</a>
    <a id="Sigma.proj₁"></a><a id="190" href="Issue982.html#190" class="Field">proj₁</a> <a id="196" class="Symbol">:</a> <a id="198" href="Issue982.html#125" class="Bound">A</a>
    <a id="Sigma.proj₂"></a><a id="204" href="Issue982.html#204" class="Field">proj₂</a> <a id="210" class="Symbol">:</a> <a id="212" href="Issue982.html#135" class="Bound">B</a> <a id="214" href="Issue982.html#190" class="Field">proj₁</a>

<a id="221" class="Keyword">open</a> <a id="226" href="Issue982.html#118" class="Module">Sigma</a> <a id="232" class="Keyword">public</a>
<a id="239" class="Markup">\end{code}</a><a id="249" class="Background">

</a><a id="251" class="Markup">\begin{code}</a>
<a id="uncurry"></a><a id="264" href="Issue982.html#264" class="Function">uncurry</a> <a id="272" class="Symbol">:</a> <a id="274" class="Symbol">{</a><a id="275" href="Issue982.html#275" class="Bound">A</a> <a id="277" class="Symbol">:</a> <a id="279" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="282" class="Symbol">}</a> <a id="284" class="Symbol">{</a><a id="285" href="Issue982.html#285" class="Bound">B</a> <a id="287" class="Symbol">:</a> <a id="289" href="Issue982.html#275" class="Bound">A</a> <a id="291" class="Symbol">→</a> <a id="293" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="296" class="Symbol">}</a> <a id="298" class="Symbol">{</a><a id="299" href="Issue982.html#299" class="Bound">C</a> <a id="301" class="Symbol">:</a> <a id="303" href="Issue982.html#118" class="Record">Sigma</a> <a id="309" href="Issue982.html#275" class="Bound">A</a> <a id="311" href="Issue982.html#285" class="Bound">B</a> <a id="313" class="Symbol">→</a> <a id="315" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="318" class="Symbol">}</a> <a id="320" class="Symbol">→</a>
          <a id="332" class="Symbol">((</a><a id="334" href="Issue982.html#334" class="Bound">x</a> <a id="336" class="Symbol">:</a> <a id="338" href="Issue982.html#275" class="Bound">A</a><a id="339" class="Symbol">)</a> <a id="341" class="Symbol">→</a> <a id="343" class="Symbol">(</a><a id="344" href="Issue982.html#344" class="Bound">y</a> <a id="346" class="Symbol">:</a> <a id="348" href="Issue982.html#285" class="Bound">B</a> <a id="350" href="Issue982.html#334" class="Bound">x</a><a id="351" class="Symbol">)</a> <a id="353" class="Symbol">→</a> <a id="355" href="Issue982.html#299" class="Bound">C</a> <a id="357" class="Symbol">(</a><a id="358" href="Issue982.html#334" class="Bound">x</a> <a id="360" href="Issue982.html#174" class="InductiveConstructor Operator">,</a> <a id="362" href="Issue982.html#344" class="Bound">y</a><a id="363" class="Symbol">))</a> <a id="366" class="Symbol">→</a>
          <a id="378" class="Symbol">((</a><a id="380" href="Issue982.html#380" class="Bound">p</a> <a id="382" class="Symbol">:</a> <a id="384" href="Issue982.html#118" class="Record">Sigma</a> <a id="390" href="Issue982.html#275" class="Bound">A</a> <a id="392" href="Issue982.html#285" class="Bound">B</a><a id="393" class="Symbol">)</a> <a id="395" class="Symbol">→</a> <a id="397" href="Issue982.html#299" class="Bound">C</a> <a id="399" href="Issue982.html#380" class="Bound">p</a><a id="400" class="Symbol">)</a>
<a id="402" href="Issue982.html#264" class="Function">uncurry</a> <a id="410" href="Issue982.html#410" class="Bound">f</a> <a id="412" class="Symbol">(</a><a id="413" href="Issue982.html#413" class="Bound">x</a> <a id="415" href="Issue982.html#174" class="InductiveConstructor Operator">,</a> <a id="417" href="Issue982.html#417" class="Bound">y</a><a id="418" class="Symbol">)</a> <a id="420" class="Symbol">=</a> <a id="422" href="Issue982.html#410" class="Bound">f</a> <a id="424" href="Issue982.html#413" class="Bound">x</a> <a id="426" href="Issue982.html#417" class="Bound">y</a>
<a id="428" class="Markup">\end{code}</a><a id="438" class="Background">

\end{document}
</a></pre></body></html>